\newcommand\hackirlabel[1]{\vspace{-20pt}\\\makebox[\linewidth][r]{\small\sc (#1)}}
\hyphenation{assign-a-bil-ity add-ing assign-able}
\newcommand{\isnew}[1]{\framebox{\ensuremath{#1}}}
% \newcommand{\mytt}[1]{{\texttt{\small #1}}}
\newcommand{\mytt}[1]{{\texttt{#1}}}
\newenvironment{verbatimfont}{\begin{small}}{\end{small}}
\newcommand{\titlett}[1]{\texttt{\large #1}}
\newcommand{\techReport}{Tech Report}
\newcommand{\readonly}{\mytt{readonly}}
\newcommand{\nro}{\mytt{nro}}
\newcommand{\mutable}{\mytt{mutable}}
\newcommand{\final}{\jv{final}}
\newcommand{\assignable}{\jv{assignable}}
\newcommand{\roOrMut}{\jv{roOrMut}}
\newcommand{\readonlyParam}[1]{\jv{readonly<#1>}}
\newcommand{\constcastkeyword}{\mytt{mutable}}
\newcommand{\thisInheritedMutability}{\jv{this-mutable}}
\newcommand{\thisInheritedAssignability}{\jv{this-assignable}}
\def\constcast#1{% applies the keyword to the arg; if no arg, just the keyword
  \def\tempa{#1}\ifx\tempa\empty{\constcastkeyword{}}%
                           \else{\mytt{(\constcastkeyword)} #1}\fi}
\newcommand{\roTemplate}{\mytt{romaybe}}
\newcommand{\roTemp}{\roTemplate{}}
\newcommand{\romaybe}{\roTemplate{}}
\newcommand{\Cconst}{\mytt{const}}
\newcommand{\Cconstcast}{\mytt{const\_cast}}
\newcommand{\Javaconst}{\mytt{const}}
\newcommand{\JACreadonly}{\mytt{readonly}}
\newcommand{\jv}[1]{\mytt{#1}}
\newcommand{\mt}[1]{\mathrm{#1}}
\newcommand{\jcmt}[1]{\rm{// #1}}
\newcommand{\addcolon}[1]{\def\tempa{#1}\ifx\tempa\empty{}\else{: #1}\fi}
\newcommand{\ok}[1]{\rm{// OK\addcolon{#1}}}
\newcommand{\cterror}[1]{\rm{// error\addcolon{#1}}}
\newcommand{\rterrortag}{RT error}
\newcommand{\rterror}[1]{\rm{// \rterrortag\addcolon{#1}}}
\makeatletter
\def\topfigrule{\kern3\p@ \hrule \kern -3.4\p@} % the \hrule is .4pt high
\def\botfigrule{\kern-3\p@ \hrule \kern 2.6\p@} % the \hrule is .4pt high
\def\dblfigrule{\kern3\p@ \hrule \kern -3.4\p@} % the \hrule is .4pt high
\makeatother
\def\floatpagefraction{.9}	% default .5
\def\dblfloatpagefraction{.9}	% default .5
\newtheorem{issue}{Issue}
\newcommand{\decision}[1]{\\ \textbf{Decision:} #1}


%%
% macros for type rules
%%

\newcommand{\code}[1]{\ensuremath{\mathtt{#1}}}
\newcommand{\mult}[1]{\overline{#1}}

\newcommand{\m}{\code{m}} % method names
\newcommand{\x}{\code{x}} % parameter name
\newcommand{\params}{\mult{\code{x}}}
\newcommand{\M}{\code{M}} % method
\newcommand{\K}{\code{K}} % constructor
\newcommand{\val}{v}      % value
% expressions
\newcommand{\e}{\code{e}} 
\newcommand{\dd}{\code{d}}
\newcommand{\expressions}{\mult{\code{e}}}
% field names
\newcommand{\f}{\code{f}}
\newcommand{\g}{\code{g}}
\newcommand{\fields}{\mult{\code{f}}}
% Class name
\newcommand{\C}{\code{C}}
\newcommand{\D}{\code{D}}
\newcommand{\E}{\code{E}}
% Types
\newcommand{\T}{\code{T}}
\newcommand{\SSS}{\code{S}}
\newcommand{\U}{\code{U}}
\newcommand{\V}{\code{V}}
\newcommand{\W}{\code{W}}
% Nonvariable types
\newcommand{\N}{\code{N}}
\newcommand{\PP}{\code{P}}
\newcommand{\Q}{\code{Q}}
% Type variable
\newcommand{\X}{\code{X}} 
\newcommand{\Y}{\code{Y}}
\newcommand{\Z}{\code{Z}}
% Javari field type
\newcommand{\F}{\code{F}} 
\newcommand{\G}{\code{G}}
\newcommand{\B}{\code{B}}  % Base type
\newcommand{\HH}{\code{H}} % Completely nonvariable type
\newcommand{\I}{\code{I}}  % Completely base type
% Weird Javari types
%\newcommand{\J}{\code{J}}
%\newcommand{\MJ}{\code{MJ}}
%\newcommand{\mpair}[2]{\pair{#1}{#2}}
%\newcommand{\add}[2]{\mathit{add}(#1, #2)}

% Type modifiers for upper and lower bounds
\newcommand{\upperBoundSyntax}{\triangleleft}
\newcommand{\lowerBoundSyntax}{\triangleright}
%\newcommand{\boundVar}{\B}
\newcommand{\dt}[2]{#1\ #2}
\newcommand{\up} [1]{#1_\upperBoundSyntax}
\newcommand{\low}[1]{#1_\lowerBoundSyntax}
\newcommand{\uplow}[1]{\dt{\up{#1}}{\low{#1}}}

\newcommand{\AF}{\code{AF}} % Assignability for fields
\newcommand{\MF}{\code{MF}} % Mutabiltiy for fields
\newcommand{\ML}{\code{ML}} % Mutability for locals
\newcommand{\AL}{\code{AL}} % Assignability for locals

% reserved types
\newcommand{\rT}{\T^*} % The type an expression evaluates to within the subject reduction rule.


% keywords
\newcommand{\new}{\code{new}}
\newcommand{\return}{\uparrow}
\newcommand{\this}{\code{this}}
\newcommand{\extends}{\mathrel{\triangleleft}}
\newcommand{\super}{\mathrel{\triangleright}}
% FJ syntax for type parametes
\newcommand{\lpa}{\mbox{\texttt{<}}}
\newcommand{\rpa}{\mbox{\texttt{>}}}

% env/store related constructs
\newcommand{\store}{\mathcal{S}}
\newcommand{\fieldRecord}{\mathcal{F}}
\newcommand{\pair}[2]{\langle #1,\ #2\rangle}
\newcommand{\pairx}[2]{#1\ #2}
\newcommand{\under}{\Delta ; \Gamma\vdash}
\newcommand{\with}[2]{[#1 \mapsto #2]}
\newcommand{\consistent}[3]{#1 ; #2 \vdash_\sigma #3}

% typing relationships
\newcommand{\subclass}{\mathrel{\!<\!:}}
\newcommand{\subclassjr}{\mathrel{\!<\!::}}
\newcommand{\subclassjrRL}{\mathrel{_R\!\!<\!::\!\!_L}}
\newcommand{\subclassjrRR}{\mathrel{_R\!\!<\!::\!\!_R}}
\newcommand{\subclassjrLL}{\mathrel{_L\!\!<\!::\!\!_L}}
\newcommand{\subclassjrLR}{\mathrel{_L\!\!<\!::\!\!_R}}
\newcommand{\jrhasType}{::}
\newcommand{\containedBy}{<=}
\newcommand{\assignto}{\rightarrow}
\newcommand{\hasType}{:}
\newcommand{\none}{\bullet}

% reduction relationships
\newcommand{\reduces}{\longrightarrow}

% Type rule aux functions
\newcommand{\fieldsfn}{\mathit{fields}}
\newcommand{\mtype}{\mathit{mtype}}
\newcommand{\mbodyfn}{\mathit{mbody}}
\newcommand{\override}{\mathit{override}}
\newcommand{\mutabilityfn}{\mathit{mutability}}
\newcommand{\mutability}[2]{\mutabilityfn(#1,\ #2)}
\newcommand{\assignabilityfn}{\mathit{assignability}}
\newcommand{\assignability}[2]{\assignabilityfn(#1,\ #2)}
\newcommand{\fieldtypefn}{\mathit{resolve}}
\newcommand{\fieldtype}[2]{\fieldtypefn(#1,\ #2)}
\newcommand{\base}[1]{\mathit{base}(#1)}
\newcommand{\lowerType}[1]{\mathit{lower}(#1)}
\newcommand{\upperType}[1]{\mathit{upper}(#1)}

% calculating bounds
\newcommand{\boundfn}{\mathit{bound}_\Delta}
\newcommand{\fboundfn}{\mathit{fbound}_\Delta}
\newcommand{\upperboundfn}{\mathit{upperBound_\Delta}}
\newcommand{\lowerboundfn}{\mathit{lowerBound_\Delta}}
\newcommand{\bound}[1]{\boundfn(#1)}
\newcommand{\fbound}[1]{\fboundfn(#1)}
\newcommand{\upperboundOne}[1]{\upperboundfn^1(#1)}
\newcommand{\upperbound}[1]{\upperboundfn(#1)}
\newcommand{\lowerboundOne}[1]{\lowerboundfn^1(#1)}
\newcommand{\lowerbound}[1]{\lowerboundfn(#1)}

% Useful macros
\newcommand{\extendsvec}[2]{\lpa\mult{\code{#1}}\extends\mult{\code{#2}}\rpa}
\newcommand{\extendsvecThree}[3]{\lpa\mult{\code{#1}}\extends\mult{\code{#2}}\super\mult{\code{#3}}\rpa}
\newcommand{\extendsvecuplow}[2]{\extendsvecThree{#1}{\up{#2}}{\low{#2}}}
\newcommand{\set}[3]{\code{set}\ #1 = #2\ \code{then}\ #3}
\newcommand{\class}[4]{\code{class}\ \code{#1}\extendsvec{#2}{#3}\extends \code{#4}\ \{ \ldots \} }
\newcommand{\newclass}[4]{\code{class}\ \code{#1}\extendsvecuplow{#2}{#3}\extends \code{#4}\ \{ \ldots \} }
\newcommand{\classB}[4]{\code{class}\ \code{#1}\extendsvec{#2}{#3}\extends \code{#4}}
\newcommand{\mbody}[3]{\code{mbody}(\code{#1}\lpa \mult{\code{#2}} \rpa,\ #3)}
\newcommand{\mbodyFour}[4]{\code{mbody}(\code{#1}\lpa \mult{\code{#2}} \rpa,\ #3\lpa \mult{#4} \rpa)}
\newcommand{\methInvk}[3]    {\code{#1}\lpa \mult{\code{#2}} \rpa(\mult{#3})}
\newcommand{\newMethInvk}[3] {\code{#1}\lpa \code{#2} \rpa(#3)}
\newcommand{\constructor}[3]{\code{#1}(\mult{\code{#2}}\ \mult{\code{#3}})\; \{\code{super}(\mult{\code{#3}});\ {\this.}\mult{\code{#3}} = \mult{\code{#3}};\}}
\newcommand{\methodDeclJava}[4]{\lpa\mult{\code{#1}} \extends \mult{\code{#2}}\rpa\ \code{#3} \ \m(\mult{\code{#3}}\ \mult{\code{#4}})\ \{\ \code{return}\ \e;\ \} }
\newcommand{\methodDeclJavari}[4]{\lpa\mult{\code{#1}} \extends \mult{\code{#2}}\rpa\ \code{#3} \ \m(\mult{\code{#3}}\ \mult{\code{#4}})\ \ML\ \{\ \code{return}\ \e;\ \} }
\newcommand{\methodDeclJavariFive}[5]{\lpa\mult{\code{#1}} \extends \mult{\code{#2}}\rpa\ \code{#3} \ \m(\mult{\code{#3}}\ \mult{\code{#4}})\ \code{#5}\ \{\ \code{return}\ \e;\ \} }
\newcommand{\sub}[2]{[#1/#2]}
\newcommand{\subvec}[2]{\sub{\mult{#1}}{\mult{#2}}}

\newcommand{\polytype}[2]{#1\lpa #2 \rpa}
\newcommand{\ptype}[2]{\polytype{#1}{\mult{#2}}}



% abbv. for toy languages
% \newcommand{\lwjava}{LW Java\xspace}
% \newcommand{\lwjavari}{LW Javari\xspace}
\newcommand{\lwjava}{LJ\xspace}
\newcommand{\lwjavari}{LJR\xspace}

\newtheorem{thm}{Theorem}
\newtheorem{lem}{Lemma}

% Smaller indentation of items.
% No vertical white space between items or paragraphs.
% Indents paragraphs as in normal text.
 \newenvironment{mydescription}
 {\begin{list}{}{
       \leftmargin \parindent
       \itemindent -\parindent
       \labelwidth 0pt
       \parsep 0pt
       \itemsep 0pt
       \listparindent \parindent
       \parskip 0pt
       \let\makelabel\descriptionlabel}}
   {\end{list}}

%%% Local Variables: 
%%% TeX-command-default: "PDF"
%%% End: 
